$\forall$${\it ds}$:$x$:Id fp$\rightarrow$ Type$_{\mbox{\scriptsize i}}$, ${\it da}$:$k$:Knd fp$\rightarrow$ Type$_{\mbox{\scriptsize i}}$. ecl(${\it ds}$;${\it da}$) $\in$ Type$_{\mbox{\scriptsize i'}}$